p:FinProbSpace. (Konig(||p||))  (nullset(p;s.True)) 

latex

Definitions

RandomVariable(p;n), x. t(x), a  b  T , {T}, SQType(T), T, suptype(S; T), i  j < k, {i..j}, , Top, A c B, i <z j, r - s, qpositive(r), p q, t.1, r + s, q_le(r;s), t.2, , gset, 1/r, r * s, b, , x f y, p  q, a < b, goset, a <p b, <+>, a < b, ff, (i = j), tt, if b then t else f fi , , P  Q, qeq(r;s), b, P  Q, S  T, t  T, r < s, (r/s), P & Q, x:A. B(x), True, A, P  Q, x:A. B(x), s  C, measure(C)  q, x(s), P  Q, Dec(P), Unit, , A  B, Konig(k), p-open(p), False, nullset(p;S), FinProbSpace, Outcome, , x  {FDLNOr12445}

Lemmas

exists functionality wrt iff, int-rational, expectation-constant, neg assert of eq int, all functionality wrt iff, nequal wf, decidable int equal, assert of le int, bnot of lt int, squash wf, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, bnot wf, le int wf, bool wf, natural number wf p-outcome, lt int wf, ifthenelse wf, assert of eq int, int seg wf, le wf, eq int wf, finite-prob-space wf, top wf, not wf, p-outcome wf, nat wf, true wf, nullset wf, length wf nat, Konig wf, p-measure-le wf, p-open-member wf, qless wf, false wf, assert-qeq, qeq wf2, assert wf, rationals wf, not functionality wrt iff, int inc rationals, qdiv wf